Nuprl Lemma : state-after-pred-ds 0,22
es:ES, ds:x:Id fp Type, e:E.
(x:Id. vartype(loc(e);x)  ds(x)?Top)
 first(e)
 state after pred(e) = (state when e)  State(ds) 
latex

Definitionst  T, x:A. B(x), loc(e), P  Q, State(ds), state@i, {T}, ES, Id, x. t(x), a:A fp B(a), E, Top, IdDeq, f(x)?z, vartype(i;x), first(e), b, A, (state when e), state after e
Lemmasnot wf, assert wf, es-first wf, es-vartype wf, fpf-cap wf, id-deq wf, top wf, es-E wf, fpf wf, Id wf, event system wf, state-after-pred, equal functionality wrt subtype rel, es-state wf, decl-state wf, es-state-subtype, es-loc wf

origin